DROPS

Document

DOI: 10.4230/LIPIcs.CONCUR.2021.15

Guard Automata for the Verification of Safety and Liveness of Distributed Algorithms

Authors: Nathalie Bertrand, Bastien Thomas, and Josef Widder

Published in: LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021)

Abstract

Distributed algorithms typically run over arbitrary many processes and may involve unboundedly many rounds, making the automated verification of their correctness challenging. Building on domain theory, we introduce a framework that abstracts infinite-state distributed systems that represent distributed algorithms into finite-state guard automata. The soundness of the approach corresponds to the Scott-continuity of the abstraction, which relies on the assumption that the distributed algorithms are layered. Guard automata thus enable the verification of safety and liveness properties of distributed algorithms.

Cite as

Nathalie Bertrand, Bastien Thomas, and Josef Widder. Guard Automata for the Verification of Safety and Liveness of Distributed Algorithms. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 15:1-15:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{bertrand_et_al:LIPIcs.CONCUR.2021.15,
  author =	{Bertrand, Nathalie and Thomas, Bastien and Widder, Josef},
  title =	{{Guard Automata for the Verification of Safety and Liveness of Distributed Algorithms}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{15:1--15:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-203-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{203},
  editor =	{Haddad, Serge and Varacca, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.15},
  URN =		{urn:nbn:de:0030-drops-143926},
  doi =		{10.4230/LIPIcs.CONCUR.2021.15},
  annote =	{Keywords: Verification, Distributed algorithms, Domain theory}
}

Search Results

Documents authored by Thomas, Bastien

Guard Automata for the Verification of Safety and Liveness of Distributed Algorithms

Abstract

Cite as

Thanks for your feedback!

Could not send message